ecl{-}trans{-}es($v$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$let $T$,${\it ks}$,$i$,$g$,$h$,$a$,$e$ = $v$ in $e$